$\forall$$A$:Realizer, $i$, $x$:Id, $T$:Type, $v$:$T$. $\neg$$x$ $\in$ dom(R{-}state($A$;$i$)) $\Rightarrow$ @$i$ $x$ initially $v$:$T$ $\parallel$ $A$